MIME-Version: 1.0
Server: CERN/3.0
Date: Monday, 06-Jan-97 21:39:25 GMT
Content-Type: text/html
Content-Length: 3826
Last-Modified: Tuesday, 16-Apr-96 18:41:34 GMT

<HTML>

<HEAD>

<TITLE>CS 395T and PHL 391</TITLE>

</HEAD><BODY bgcolor="ffffff">

<BODY>

<h2>CS 395T and PHL 391, Spring 1996, <em>Foundations of
Mathematics</em>, TT 2:00-3:30, Taylor 3.144</h2>

<UL>


<LI> Course blurb: There are many approaches to formal reasoning.  The
objective of specifying computer programs, including the formalization
of worlds with which programs are to interact, has led to the creation
of numerous tools for formal reasoning.  We will examine some systems
for formal reasoning while examining a number of mechanical formal
methods tools that support these different systems.  Examples of such
system/tool pairs are: 

<p> <pre>

 System                           Tool
				
 Primitive Recursive Arithmetic   Boyer-Moore Prover, ACL2
 First Order Logic                Otter, Nelson's qed
 Higher Order Logic               HOL, IMPS
 Equational Reasoning             OBJ
 Set Theory                       Mizar, Quaife/Otter, PVS
 Type Theory                      NuPrl, Lego, Coq

</pre>
<p>
Students will choose, with the help of the instructor, a system and/or
tool to examine and the grade will be based upon presentations about
these.

<p><LI><!WA0><a href="http://www.mcs.anl.gov/qed/index.html"> The QED Project
</a>

<UL>

<LI>HTML Version of <!WA1><a
href="http://www.cybercom.net/~rbjones/rbjpub/logic/qedres00.htm">the
QED Manifesto</a>

<LI>Plain text version of <!WA2><a
href="ftp://ftp.cs.utexas.edu/pub/boyer/qed-manifesto">the QED
Manifesto</a>

</UL>

<p><LI><!WA3><a href="http://www.comlab.ox.ac.uk/archive/formal-methods.html">
Bowen' Formal Methods Web Page</a> and a <!WA4><a href="http://www.cs.utexas.edu/users/boyer/courses/backup-formal-methods.html">
backup copy</a>.



<p><LI>The chief assignment.  Select a formal methods system, e.g.,
from Bowen's Formal Methods Web Page above, and report via in-class,
oral presentations on either its logical foundations or upon its use.
Many of these systems have good, freely available implementations.
Consult with me before making a final choice.

<p><LI>No tests, no final.  Only the presentation(s).

<p><LI>I hope to have a number of guest presentations from the local
formal methods community.

</UL>

<p><LI>*Very* Tentative Schedule
<UL>

<!
 Jan 30 -- Matt Wilding on Nqthm proofs about the Clinc Stack and
the Nim program

 Feb 1 -- Matt Wilding on Nqthm proofs about real time programs

 Feb 6 -- Carl Pixley (Motorola) Formal Verification of Hardware:
Hardware Models; CTL Language; BDD implementation of model checking;
Industrial use:  Abstract modelling, Implementation modelling



Feb 8 -- J Moore (Computational Logic) Overview of ACL2 and
its relationship to Common Lisp



Feb 13 -- Matt Kaufmann (Motorola) Tutorial examples of ACL2 use

Feb 15 --  J Moore (Computational Logic) Advanced ACL2 applications



Feb 20 -- Strongly urge attendance at an Ed Clarke talk this week
(He will be giving a talk on Monday, Feb. 19th in Taylor 3.128 from
2:00-3:00 and on Wednesday, Feb. 21st in Taylor 3.128 from 1:30-2:30.)

Feb 22 -- Warren Hunt (Computational Logic) FM9001 Verification

Feb 27 -- Warren Hunt (Computational Logic) FM9001 Verification

Feb 29 -- Jun Sawada

March 5 -- Matt Wilding



March 7 -- Ruben Gamboa

March 12 -- Spring Break

March 14 -- Spring Break

March 19 -- Jun Sawada continues

March 21 -- Carl Pixley (Motorola) CTL

March 26 -- Markus Kaltenbach

March 28 -- Kenneth Chen -- Otter

April 2 -- Patrick Ray -- Larch

April 4 -- Larry Hines (UT and EDS) -- A set theory prover

April 9 -- William Adams -- Type theory

April 11 -- Rick Tanney  -- Coq

>

<LI> April 16 -- Rick Tanney  -- Coq continued

<LI> April 18 -- Trevor Hicks -- Otter

<LI> April 23 -- Ruben Gamboa on ACL2 and Square root of 2

<LI> April 25 -- Samuel Guyer -- Circal and process algebras

<LI> April 30 -- Sawada -- PVS

<LI> May 2 -- Russell Turpin (SES) -- Galois

</UL>



